COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(wipe-out)
C00003 00003	EKL did it first, but cannot do it now
C00004 00004	PDL-OVERFLOW occurs also at line 3 of the proof DIAGONALIZE in the file 
C00005 00005	    (proof sets)
C00007 ENDMK
C⊗;
(wipe-out)
(get-proofs mult)

(proof multsum)

(ue (phi |λu. disj_pair(a,b)⊃mult(u,a∪b)=mult(u,a)+mult(u,b)|) listinduction
    (part 1 (open mult union disj_pair emptyp intersection) 
            (use normal mode: always))
        (part 1 (der)) )
(label multsum)

(setq rewritemessages t)
;EKL did it first, but cannot do it now
(wipe-out)
(get-proofs sums)
(proof unionprop)

(setq rewritemessages t)

(ue (a |λn.n≤length u⊃
                (un(λm.mkset(nth(u,m)),n))(x)≡some(n,λk.nth(u,k)=x)|)
    proof_by_induction (part 1(open un mkset nth some union emptyset) (der))
    (use trans_lesseq succ_lesseq_lesseq))
;∀N.N≤LENGTH U⊃(UN(λM.MKSET(NTH(U,M)),N))(X)≡SOME(N,λK.NTH(U,K)=X)

;;PDL-OVERFLOW
QUIT


;;PDL-OVERFLOW occurs also at line 3 of the proof DIAGONALIZE in the file 
;ramsey[ekl,sys]
    (proof sets)

1.  (decl (av bv) (type: |ground→truthval|))
2.  (decl epsilon (type: |ground⊗@set→truthval|) 
             (infixname: ε) (bindingpower: 925))
   ;SET is an unknown atom in type (GROUND⊗(@SET))→TRUTHVAL

3.  (define epsilon |∀a xv.xvεa≡a(xv)|)
    (label epsilondef)

;A is unknown.
;XV is unknown.
;EPSILON is unknown.
;the symbol EPSILON declared to have type ((GROUND→TRUTHVAL)→TRUTHVAL)→GROUND
;the symbol XV declared to have type GROUND→TRUTHVAL
;the symbol A declared to have type (GROUND→TRUTHVAL)→TRUTHVAL
;weird error in type computation - tell jk: the type 
GROUND should have been an appl type.